COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	propositional schemata, used by the rewriter to normalize expressions
C00004 ENDMK
C⊗;
;propositional schemata, used by the rewriter to normalize expressions
(wipe-out)
(proof normal)

(axiom  |∀p q r.((p∨q)∧r)≡((p∧r)∨(q∧r))|)
(label normal)
(axiom  |∀p q r.(r∧(p∨q))≡((r∧p)∨(r∧q))|)
(label normal)
(axiom  |∀p q r.(r∧(p∨q))≡((p∧r)∨(q∧r))|)
(label normal)
(axiom |∀p q r.(p∨q⊃r)≡(p⊃r)∧(q⊃r)|)
(label normal)

(axiom  |∀p q.(¬(p∨q))≡((¬p)∧(¬q))|)
(label demorgan)

(axiom |∀P Q.¬(P∧Q)≡¬P∨¬Q|)
(label demorgan1)

;It would cause combinatorial explosion,to add these to simpinfo, or to put everything,
;say,in conjunctive normal form. So we call them as rewriters when needed.

;a few tricks

(axiom |∀p q.p≡(q⊃p)∧(¬q⊃p)|)
(label excluded_middle)

(derive |∀p q r.(q⊃r)∧(if p then q else r)⊃r|)
(label trans_cond)
(save-proofs normal)